-
Notifications
You must be signed in to change notification settings - Fork 80
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Rust constr enum #1941
Rust constr enum #1941
Conversation
ast/src/analyzed/mod.rs
Outdated
} | ||
} | ||
|
||
// TODO This is the only version of Identity left. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@chriseth can I remove this comment?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The idea behind this comment was to refactor Identity so that it is only generic over the field, and not about what a selected expressions or an expression / algebraic expression is. If you did this change, then you can remove it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh I didnt get that but yes that's exactly what I did :)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you remove the TODO?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
done
@@ -309,6 +336,9 @@ fn all_row_connected_witnesses<T>( | |||
witnesses.extend(in_rhs); | |||
} | |||
} | |||
Identity::Permutation(..) | Identity::Connect(..) => { | |||
todo!("same as plookup, avoid repetition?") | |||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The comment of this function does not mention connect, is this something we use?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Connect is very sporadically implemented.
@@ -227,7 +228,13 @@ impl<'a, 'b, T: FieldElement> WitnessGenerator<'a, 'b, T> { | |||
// as they are assumed to be handled in stage 0. | |||
let polynomial_identities = identities |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is it possible for identities
to still contains anything else than polynomial identities? If so, due to the filtering these would get ignored? Or do we not have any non-polynomial identities, in which case this can be a hard cast rather than a filter?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the filtering here could be improved in general. I don't see polynomial constraints between lower-stage witness column being filtered out, for example. I also don't see a reason why this should only contain polynomial constraints at this stage, e.g. we shouldn't filter out the lookups. Of course, usually when we use a multi-stage approach the idea is to remove the lookups, but conceptually, we could still have a lookup at a higher stage (although the backend probably would not support it).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How about we leave this as is in this PR?
ast/src/analyzed/mod.rs
Outdated
} | ||
} | ||
|
||
pub fn source(&self) -> &SourceRef { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There is a trait called SourceReference, I think we should implement that instead.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
executor/src/witgen/machines/mod.rs
Outdated
Permutation, | ||
} | ||
|
||
impl<'a, T> ConnectingIdentityRef<'a, T> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there any way we could re-write the code that uses these Refs so that they are not needed?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm.. So assuming we only rely on the overlap of the two (left and right selected expressions) we could just pass that, but I don't really find that cleaner and we lose the ability to do things specifically for each case.
Also this assumption doesn't seem to hold since we have code like this for WriteOnceMemory
if !parts.connecting_identities.values().all(|i| i.is_lookup()) {
return None;
}
Or this for BlockMachine
// Connecting identities should either all be permutations or all lookups.
let connection_type = connecting_identities
.values()
.map(|id| id.kind())
.unique()
.exactly_one()
.ok()?;
If your point is that we could refactor these, maybe? I think the current way turns what was a runtime invariant into a compile-time one, with minimal changes to the rest of the code.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we are not talking about the same thing. My question was if we can avoid adding a ..Ref
type for every type.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok then I don't understand, there's a single Ref type and it's ConnectingIdentityRef
. It exists because connecting identities can only be of certain types, so using &'a Identity
would lead to a bunch of unreachable!()
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah sorry, I thought this was the code used in path canonicalizer which is also sprinkled with ...Refs.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't really like it either to be honest.
What about
struct ConnectingIdentity<'a, T> {
left: &'a SelectedExpressions<T>,
right: &'a SelectedExpressions<T>,
kind: ConnectingIdentityKind
}
Where kind
is Lookup
or Permutation
and will not need to be extended for PhantomLookup
and PhantomPermutation
?
Then we can remove some duplicated code and still rely on kind
for the cases I pointed out above?
I don't really see how traits help here, since at the end of the day we need to be able to store either of these two possibilities anywhere, so we'd have to use dyn ConnectingIdentity
which seems unnatural here due to the fixed number of variants. But maybe I'm not zooming out enough here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I tried the above and I like it more
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Cool! Don't we need the ID? Oh, it's in a hash map from id anyway, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah I put the id for now but it did seem redundant, let's see.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's gone!
pilopt/src/lib.rs
Outdated
struct CanonicalIdentity<'a, T>(&'a Identity<T>); | ||
|
||
impl<T: PartialEq> PartialEq for CanonicalIdentity<'_, T> { | ||
fn eq(&self, other: &Self) -> bool { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
At least this one can be implemented using PartialOrd, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Excellent point
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done using Ord
Reverting to draft as I realised I broke |
// Set of (left, right) tuples. | ||
let mut identity_expressions = BTreeSet::new(); | ||
let to_remove = pil_file | ||
.identities | ||
.iter() | ||
.enumerate() | ||
.filter_map(|(index, identity)| { | ||
match identity_expressions.insert((&identity.left, &identity.right)) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
By the way, this seems like a bug, as these would be considered duplicates:
[a] in [b]
[a] connect [b]
[a] is [b]
I don't see that typically happening but still.
) => a.cmp(b), | ||
( | ||
Identity::Lookup(LookupIdentity { | ||
left: a, right: b, .. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You could use a generic left
and right
function for any non-polynomial identity.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I thought about it but given that these are in different variants, I don't see how we could use it:
now we have:
Identity::Lookup(LookupIdentity { left, right, .. }) | Identity::Permutation(PermutationIdentity { left, right, ..}) => {
left
}
With a trait, we can't treat both variants at the same time because we can only bind to variables of the same type in patterns:
// does NOT work
Identity::Lookup(i) | Identity::Permutation(i) => {
i.left()
For this to be possible, we need to use the same struct inside the variant:
Identity::Lookup(ConnectingIdentity<Lookup>),
Identity::Permutation(ConnectingIdentity<Permutation>),
... but this doesn't work either because the generic types also need to match!
So we go one step further and use the same variant
Identity::Connection(ConnectingIdentity)
And store the kind inside the ConnectingIdentity
.
This is nice but my issue is that at this point we drifted away completely from the PIL enum.
My conclusion is that relying on patterns to work across connecting identities, while verbose, is fine as it preserves the structure of the PIL enum. If we refactor the PIL enum to be nested, then the nested approach would work in Rust as well. I don't think this refactor is necessarily beneficial (because of its nested nature), nor a priority.
executor/src/witgen/machines/mod.rs
Outdated
Permutation(&'a PermutationIdentity<T>), | ||
} | ||
|
||
impl<'a, T: Display> Display for ConnectingIdentityRef<'a, T> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could use derive_more
here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
done
// For lookups, any lookup calling from the current machine belongs | ||
// to the machine; lookups to the machine do not. | ||
let all_refs = &refs_in_selected_expressions(&i.left) & (&all_witnesses); | ||
let all_refs = match i { | ||
Identity::Polynomial(identity) => { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe extract that into a function?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
done, with all_children
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That was wrong so done, just extracting as suggested
.filter_map(|i| { | ||
let id = i.id(); | ||
match i { | ||
Identity::Polynomial(_) => None, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe extract that into a function?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
simplified due to refactor of ConnectingIdentity
This is ready for another review @chriseth |
ast/src/analyzed/mod.rs
Outdated
} | ||
|
||
impl<T> PolynomialIdentity<T> { | ||
pub fn new(id: u64, source: SourceRef, expression: AlgebraicExpression<T>) -> Self { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we acutally need this when the fields are all pub
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, personal preference but happy to remove these especially since we rely heavily on destructuring anyway
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
removed
executor/src/witgen/machines/mod.rs
Outdated
@@ -151,6 +150,67 @@ impl<'a, T: FieldElement> Machine<'a, T> for KnownMachine<'a, T> { | |||
} | |||
} | |||
|
|||
#[derive(Clone, Copy)] | |||
pub struct ConnectingIdentity<'a, T> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe one line of documentation?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
done
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hm, not sure I would agree to this. A polynomial identity can also cross machine boundaries (depending on the definition, it would be the same machine, but still...). Shouldn't we be more explicit about the kind? Or the fact that it has two parts that do not need to match on the same row or something like that if you want to be abstract?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would just be explicit and say, lookup or permutation.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I still think the doc is confusing (people will wonder if it is related to Identity or not), but ok.
Identity
is currently a struct which acts as an union: all kinds of identities are represented using the same struct fields, with runtime checks that the right fields are used.In the context of #1934 where we add new kinds of identities, it seems advantageous to move to an enum on the Rust side as well.
Todo: